Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

fix: break the functor Run into Run and TryWith #97

Merged
merged 7 commits into from
Jul 31, 2022
Merged

fix: break the functor Run into Run and TryWith #97

merged 7 commits into from
Jul 31, 2022

Conversation

favonia
Copy link
Collaborator

@favonia favonia commented Jul 30, 2022 •
edited
Loading

This is a breaking change!

This is an alternative to the PR #96 without using first-class modules. It is practically backward-compatible because none of our new proof assistants have implemented the (planned) features that will need try_with yet (and I believe we are still the only users of this otherwise super cool library).

The documentation of try_with has been rewritten, though the wording is still a bit awkward.

@favonia favonia requested a review from jonsterling July 30, 2022 12:57
@favonia favonia mentioned this pull request Jul 30, 2022
Closed
jonsterling
jonsterling approved these changes Jul 31, 2022
View reviewed changes
Copy link
Contributor

@jonsterling jonsterling left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It looks fine, but I'd like to better understand something. In Discord you mentioned that it doesn't make conceptual sense for these two to be part of the same module functor --- but in the documentation I think I see that the intended use-case is that you will use try_with to tweak some effects within the dynamic scope of a call to run. So it sounds like these do go hand-in-hand, though I understand that maybe Run is not the best name for the functor.

I'm ok with separating them, but I just wanted to better understand the choice.

src/ScopeSigs.ml Show resolved Hide resolved
@favonia
Copy link
Collaborator Author

favonia commented Jul 31, 2022 •
edited
Loading

It is very subtle. When we are writing the code

let module R = S.Run (H) in
R.run f (* <-- this line *)

the function R.try_with is also available on the last line, along with R.run, but it does not make sense. The functorial interface before this PR makes both run and try_with available at the same time for the same H, but for any realistic H almost only one of them makes sense: the H that works for run should not be used for try_with and vice versa. After this PR, the user must make a clear choice when applying the functor to H. They have to choose between S.Run (H) and S.TryWith (H), and only one of run and try_with will be available.

@jonsterling
Copy link
Contributor

Now i understand! thank you

@jonsterling
Copy link
Contributor

Now I see how silly my question was! Thanks for answering it anyway 😆

@favonia favonia merged commit 3ac136c into main Jul 31, 2022
@favonia favonia deleted the separate-run-and-try_with branch July 31, 2022 15:54
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@jonsterling jonsterling jonsterling approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@favonia @jonsterling